In software development, a great deal of effort is spent on trying to specify software requirements and on ensuring that software actually matches these requirements. A wide range of techniques have been proposed, including theorem proving, model checking, type-based analysis, static analysis, runtime monitoring and the like. However, in many areas, adoption of these techniques remains inconsistent.
Obtaining a specification or a precise notion of correctness based on a verbal or written description of a programming task in many cases is quite elusive. For example, for many tasks, even expert programmers are unable to get programming tasks correct because of numerous “corner cases”that are often difficult to recognize.
For example, consider coming up with a regular expression to recognize valid email addresses, or to sanitize an input string to avoid SQL injection attacks. Both of these tasks are easy to describe to most developers succinctly, yet both are difficult to implement properly, because of the need to address tricky corner cases. Furthermore, there is room for ambiguity in both tasks; for example, even experienced developers can disagree as to whether john+doe@acm:org or john::doe:@acm:com are valid email addresses, or whether removing all characters outside of the a through z and A through Z set is a valid sanitization strategy for SQL injections. Such examples show how programming tasks are typically under-specified, and that they may not have absolute consensus on what solution is correct. Moreover, different people may get different parts of the task wrong.